$\forall$$A$, $B$:(Id$\rightarrow$MsgA), $l$:IdLnk, ${\it tg}$:Id. interface{-}link($A$;$B$;$l$;${\it tg}$) $\in$ Prop